T:Type, l:(T List). (||l|| = 0)  (l = []) 

latex

Definitions	prop{i:l}, t  T, P  Q, P  Q, P  Q, Y, ||as||, P  Q, x:A. B(x), False, A, P  Q, decidable(P)
Lemmas	length wf1, non neg length, decidable int equal